package de.unibi.comet.fa;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Map.Entry;

import de.unibi.comet.util.BitArray;
import de.unibi.comet.util.Log;

/** Represents a counting deterministic finite automaton. */
public class CDFA {
	private List<int[]> transitionTable;
	private List<Integer> outputTable;
	
// 	private List<CDFANode> nodeTable; 
	private Alphabet alphabet;
	
	/** Constructor.
	 *  @param transitionTable List that contains one entry for each state, where an entry is
	 *    a array of integers of size alphabet.size(), i.e. transitionTable.get(state)[char] 
	 *    gives the target state for a transition from "state" under "char". 
	 */
	public CDFA(Alphabet alphabet, List<int[]> transitionTable, List<Integer> outputTable) {
		this.alphabet = alphabet;
		this.transitionTable = transitionTable;
		this.outputTable = outputTable;
	}
	
	/** Count matches.
	 *  @return Returns number of times the automaton was in an accept state.
	 *     Returns -1 if string led to an invalid state. */
	public int countMatchesDFA(String s) {
		Log.getInstance().startTimer();
		int unknownIndex = alphabet.getIndex('#');
		
		int node = 0;
		int count = outputTable.get(0);
		for (int i=0; i<s.length(); ++i) {
			int c = alphabet.getIndex(s.charAt(i));
			// map all other (those not in the pattern) characters onto #
			if (c<0) {
				if (unknownIndex>=0) c=unknownIndex;
				else throw new IllegalArgumentException(String.format("Unknown character \"%s\" encountered", c));
			}
			
			node = transitionTable.get(node)[c];
			if (node<0) return -1;
			
			// Log.getInstance().printInsane(String.format("%d(%s): %d", i, c, node.getIndex()));
			count+=outputTable.get(node);
//			if (node.getOutput()>0) {
//				Log.getInstance().printInsane(String.format("m %d (state: %d)", i, node.getIndex()));
//			}
		}
		Log.getInstance().stopTimer("dfa matching");
		return count;
	}
	
	/** Minimize the CDFA. */
	public CDFA minimize() { return minimizeHopcroft(); }
	
	/** Minimize the CDFA using Hopcroft's algorithm. */
	public CDFA minimizeHopcroft() {
		Log.getInstance().startTimer();
		int maxBlocks = outputTable.size();
		// step 1) construct inverse transition function
		InverseTransitionFunction inverse = new InverseTransitionFunction(transitionTable, alphabet.size());
		// step 2) partition to start with is given by output table
		Partition partition = new Partition(outputTable);
		// step 3) construct statesWithInverses[blockIdx][character]
		@SuppressWarnings("unchecked")
		List<Integer>[][] statesWithInverses = new List[maxBlocks][alphabet.size()];
		for (int block : partition.blockIndices()) {
			for (int c=0; c<alphabet.size(); ++c) {
				List<Integer> l = new ArrayList<Integer>();
				for (int state : partition.block(block)) {
					if (inverse.hasInverse(state, c)) l.add(state);
				}
				if (l.size()>0) statesWithInverses[block][c]=l;
			}
		}
		// step 4) create job list
		@SuppressWarnings("unchecked")
		LinkedList<Integer>[] toCheck = new LinkedList[alphabet.size()];
		// BitArray to fastly determine if a block is in the list.
		BitArray[] toCheckBitArrays = new BitArray[alphabet.size()];
		for (int c=0; c<alphabet.size(); ++c) {
			toCheck[c]=new LinkedList<Integer>();
			toCheckBitArrays[c]=new BitArray(maxBlocks);
			for (int block : partition.blockIndices()) {
				if (statesWithInverses[block][c]==null) continue;
				toCheck[c].add(block);
				toCheckBitArrays[c].set(block, true);
			}
		}
//		for (int c=0; c<alphabet.size(); ++c) {
//			// find largest set
//			int max = Integer.MIN_VALUE;
//			int maxIndex = -1;
//			for (int block : partition.blockIndices()) {
//				if (statesWithInverses[block][c]==null) continue;
//				if (statesWithInverses[block][c].size()>max) {
//					max=statesWithInverses[block][c].size();
//					maxIndex=block;
//				}
//			}
//			// now populate toCheck
//			toCheck[c]=new LinkedList<Integer>();
//			toCheckBitArrays[c]=new BitArray(maxBlocks);
//			for (int block : partition.blockIndices()) {
//				if (block==maxIndex) continue;
//				if (statesWithInverses[block][c]==null) continue;
//				toCheck[c].add(block);
//				toCheckBitArrays[c].set(block, true);
//			}
//			// TODO: this can lead to empty lists, is that correct? maybe do this: 
//			if (toCheck[c].isEmpty() && (maxIndex>=0)) {
//				toCheck[c].add(maxIndex);
//				toCheckBitArrays[c].set(maxIndex, true);
//			}
//		}
		// step 5) main iteration
		int character = 0;
		@SuppressWarnings("unchecked")
		LinkedList<Integer>[] statesToSplitOff = new LinkedList[maxBlocks];
		while (true) {
			int block=-1;
			for (int i=0; i<alphabet.size(); ++i) {
				if (toCheck[character].size()>0) {
					block=toCheck[character].remove();
					toCheckBitArrays[character].set(block, false);
					break;
				}
				character=(character+1)%alphabet.size();
			}
			if (block==-1) break;
			// check which states have to be split off their blocks
			if (statesWithInverses[block][character]==null) continue;
			LinkedList<Integer> blocksToSplit = new LinkedList<Integer>();
			for (int stateWithInverse : statesWithInverses[block][character]) {
				for (int stateToBeSplitOff : inverse.get(stateWithInverse, character)) {
					int blockToSplit = partition.getBlockIndex(stateToBeSplitOff);
					if (statesToSplitOff[blockToSplit]==null) {
						blocksToSplit.add(blockToSplit);
						statesToSplitOff[blockToSplit]=new LinkedList<Integer>();
					}
					statesToSplitOff[blockToSplit].add(stateToBeSplitOff);
				}
			}
			// perform the split
			for (int blockToSplit : blocksToSplit) {
				// dont split if whole block is to be split off (which wouldnt be a split at all)
				if (statesToSplitOff[blockToSplit].size()==partition.blockSize(blockToSplit)) {
					// TODO: add something here?
					statesToSplitOff[blockToSplit]=null;
					continue;
				}
				// perform the split
				int newBlock = partition.splitOff(statesToSplitOff[blockToSplit]);
				// recalculate statesWithInverse for the two modified blocks
				int[] changedBlocks = {blockToSplit, newBlock};
				for (int i : changedBlocks) {
					for (int c=0; c<alphabet.size(); ++c) {
						List<Integer> l = new ArrayList<Integer>();
						for (int state : partition.block(i)) {
							if (inverse.hasInverse(state, c)) l.add(state);
						}
						if (l.size()>0) statesWithInverses[i][c]=l;
						else statesWithInverses[i][c]=null;
					}
				}
				// update toCheck
				for (int c=0; c<alphabet.size(); ++c) {
// conservative variant:
//					toCheck[c].add(newBlock);
//					toCheckBitArrays[c].set(newBlock, true);
//					if (!toCheckBitArrays[c].get(blockToSplit)) {
//						toCheck[c].add(blockToSplit);
//						toCheckBitArrays[c].set(blockToSplit, true);						
//					}
					if (toCheckBitArrays[c].get(blockToSplit)) {
						toCheck[c].add(newBlock);
						toCheckBitArrays[c].set(newBlock, true);
					} else {
						int i1 = statesWithInverses[blockToSplit][c]==null?0:statesWithInverses[blockToSplit][c].size();
						int i2 = statesWithInverses[newBlock][c]==null?0:statesWithInverses[newBlock][c].size();
						if (i1<=i2) {
							toCheck[c].add(blockToSplit);
							toCheckBitArrays[c].set(blockToSplit, true);							
						} else {
							toCheck[c].add(newBlock);
							toCheckBitArrays[c].set(newBlock, true);							
						}
					}
				}
				statesToSplitOff[blockToSplit]=null;
			}
		}

		// finally construct new automaton
		// map from block index to new state number
		HashMap<Integer,Integer> stateMap = new HashMap<Integer,Integer>(2*outputTable.size());
		int n=0;
		for (int i=0; i<outputTable.size(); ++i) {
			int block = partition.getBlockIndex(i);
			if (stateMap.get(block)==null) stateMap.put(block, n++);
		}
		// create new output table
		Integer[] newOutputTable = new Integer[partition.blockCount()];
		List<int[]> newTransitionTable = new ArrayList<int[]>(partition.blockCount());
		for (int i=0; i<outputTable.size(); ++i) {
			int block = partition.getBlockIndex(i);
			int newState = stateMap.get(block);
			if (newOutputTable[newState]!=null) continue;
			int oldState = partition.block(block).iterator().next();
			newOutputTable[newState]=outputTable.get(oldState);
			int[] t = new int[alphabet.size()];
			for (int c=0; c<alphabet.size(); ++c) {
				int targetBlock = partition.getBlockIndex(transitionTable.get(oldState)[c]); 
				t[c] = stateMap.get(targetBlock);
			}
			newTransitionTable.add(t);
		}
		
		Log.getInstance().printInsane(String.format("minimization (hopcroft): %d states", partition.blockCount()));
		Log.getInstance().stopTimer("minimize automaton (hopcroft)");
		
		return new CDFA(alphabet, newTransitionTable, Arrays.asList(newOutputTable));
	}

	/** Perform DFA minimization according to "Kozen, Automata and Compatibility".
	 *  Assumes that this is a DFA. */
	public CDFA minimizeKozen() {
		Log.getInstance().startTimer();
		int nodeCount = outputTable.size();
	
		/** Set entry to true if the two nodes are not equivalent. */
		BitArray[] notEquivalent = new BitArray[nodeCount];
		// create (triangle) matrix
		for (int i=0; i<nodeCount; ++i) {
			notEquivalent[i]=new BitArray(i);
		}
		// initialize 
		// TODO: more efficient using bucket-something
		for (int i=0; i<nodeCount; ++i) {
			for (int j=0; j<i; ++j) {
				if (outputTable.get(i)!=outputTable.get(j)) {
					notEquivalent[i].set(j, true);
				}
			}
		}
		// main loop: build equivalence table
		boolean changeMade = true;
		while (changeMade) {
			changeMade = false;
			for (int i=0; i<nodeCount; ++i) {
				for (int j=0; j<i; ++j) {
					if (notEquivalent[i].get(j)) continue;
					for (int c=0; c<alphabet.size(); ++c) {
						int tI = this.transitionTable.get(i)[c];
						int tJ = this.transitionTable.get(j)[c];
						if (tI==tJ) continue;
						if (tI<tJ) {
							int tmp = tI;
							tI=tJ;
							tJ=tmp;
						}
						if (notEquivalent[tI].get(tJ)) {
							notEquivalent[i].set(j, true);
							changeMade=true;
							continue;
						}
					}
				}
			}
			
//			for (int i=0; i<notEquivalent.length; ++i) {
//				StringBuffer sb = new StringBuffer();
//				sb.append(String.format("%03d: ", i));
//				for (int j=0; j<i; ++j) {
//					sb.append(String.format("%d, ", notEquivalent[i].get(j)?1:0));
//				}
//				Log.getInstance().printInsane(sb.toString());
//			}
		}
		// create table to know which nodes should be substituted by others
		int substitutionTable[] = new int[nodeCount];
		int[] nodeMap = new int[nodeCount];
		for (int i=0; i<nodeCount; ++i) substitutionTable[i]=-1;
		int nodesNeeded = 0;
		for (int i=0; i<nodeCount; ++i) {
			if (substitutionTable[i]!=-1) continue;
			nodeMap[i]=nodesNeeded;
			++nodesNeeded;
			// use -2 to indicate that current node is to be used as representant for
			// equivalence class (because its the node in this class with the lowest
			// index)
			substitutionTable[i]=-2;
			// check which of the rest of the nodes fall into this equivalence class
			for (int j=i+1; j<nodeCount; ++j) {
				if (!notEquivalent[j].get(i)) substitutionTable[j]=i;
			}
		}
		// create new node table
		Integer[] newOutputTable = new Integer[nodesNeeded];
		List<int[]> newTransitionTable = new ArrayList<int[]>(nodesNeeded);
		int n = 0;
		for (int i=0; i<nodeCount; ++i) {
			if (substitutionTable[i]!=-2) continue;
			newOutputTable[n]=outputTable.get(i);
			int[] transitions = new int[alphabet.size()];
			for (int c=0; c<alphabet.size(); ++c) {
				int originalTarget = transitionTable.get(i)[c];
				int k = (substitutionTable[originalTarget]==-2)?originalTarget:substitutionTable[originalTarget];
				transitions[c]=nodeMap[k];
			}
			newTransitionTable.add(transitions);
			++n;
		}

		Log.getInstance().printEverything(String.format("minimization (kozen): %d", nodesNeeded));
		Log.getInstance().stopTimer("minimize automaton (kozen)");
		
		return new CDFA(alphabet, newTransitionTable, Arrays.asList(newOutputTable));
//		for (int i=0; i<notEquivalent.length; ++i) {
//			StringBuffer sb = new StringBuffer();
//			sb.append(String.format("%03d: ", i));
//			for (int j=0; j<i; ++j) {
//				sb.append(String.format("%d, ", notEquivalent[i].get(j)?1:0));
//			}
//			Log.getInstance().printInsane(sb.toString());
//		}
//
//		StringBuffer sb = new StringBuffer();
//		sb.append("substitutionTable: ");
//		for (int i=0; i<substitutionTable.length; ++i) {
//			sb.append(String.format("%d:%d, ", i, substitutionTable[i]));
//		}
//		Log.getInstance().printInsane(sb.toString());
	}

	/** Greatest common divisor. */
	static private int gcd(int a, int b) {
		if (a<b) return gcd(b,a);
		while (b!=0) {
			int tmp=b;
			b=a%b;
			a=tmp;
		}
		return a;
	}

	/** Experimental method that outputs the periodicity of each state and returns
	 *  the number of states with periodicity!=0. */
	public int analysePeriodicity() {
		int result = 0;
		// loop over all states and analyze for each its periodicity
		for (int state=0; state<transitionTable.size(); ++state) {
			List<Integer> tmpList = new ArrayList<Integer>();

			int period = -1;
			HashSet<Integer> reachable = new HashSet<Integer>();
			reachable.add(state);
			int n = 0;
			while ((period!=1) && (n<1000)) {
				HashSet<Integer> nextReachable = new HashSet<Integer>();
				for (int i : reachable) {
					for (int j : transitionTable.get(i)) nextReachable.add(j);
				}
				++n;
				reachable=nextReachable;
				if (reachable.contains(state)) {
					if (period==-1) {
						period=n;
					} else {
						period=gcd(n,period);
					}
					tmpList.add(n);
				}
			}
			StringBuffer sb = new StringBuffer();
			sb.append(String.format("%d: %d (", state, period));
			for (int i : tmpList) {
				sb.append(i);
				sb.append(',');
			}
			sb.append(')');
			System.out.println(sb.toString());
			if (period!=1) ++result;
		}
		return result;
	}

	/** Naive (slow) approach to asymptotic equivalence.
	 *  WARNING: This is experimental stuff.
	 */
	public Partition analyseAsymptoticEquivalence() {
		// determinte final states
		BitArray finalStates = new BitArray(transitionTable.size());
		for (int state=0; state<outputTable.size(); ++state) {
			if (outputTable.get(state)==0) continue;
			if (outputTable.get(state)==1) {
				finalStates.set(state, true);
			} else {
				throw new IllegalStateException("Not implemented for output(state)>1");
			}
		}
		
		// for each state the lengths of the strings leading to a final state
		BitArray[] lengthsArray = new BitArray[transitionTable.size()];
		final int maxLength = 63;
		
		// loop over all states and analyze for each its periodicity
		for (int state=0; state<transitionTable.size(); ++state) {
			// set of states currently active
			BitArray stateSet = new BitArray(transitionTable.size());
			stateSet.set(state, true);
			// possible lengths of strings leading from current state to a final state
			BitArray lengths = new BitArray(maxLength+1);
			if (finalStates.get(state)) lengths.set(0, true);
			
			// true if the state does not change any more
			boolean stable = false;
			for (int i=1; i<=maxLength; ++i) {
				// update state set
				if (!stable) {
					BitArray newStateSet = new BitArray(transitionTable.size());
					int sourceState = -1;
					for (boolean b : stateSet) {
						++sourceState;
						if (!b) continue;
						for (int targetState : transitionTable.get(sourceState)) newStateSet.set(targetState, true); 
					}
					if (newStateSet.equals(stateSet)) {
						stable=true;
					} else {
						stateSet=newStateSet;
					}
				}
				// check if we are in a final state
				BitArray tmp = new BitArray(stateSet);
				tmp.and(finalStates);
				if (!tmp.allZero()) lengths.set(i, true);
			}
			if (!stable) throw new IllegalStateException("State set did not stabelize, increase \"maxLength\"");
			lengthsArray[state]=lengths;
			
			StringBuffer sb = new StringBuffer();
			sb.append(String.format("%d: ", state));
			int m=maxLength;
			for (; m>=1; --m) {
				if (!lengths.get(m-1)) break;
			}
			int n = 0;
			for (boolean b : lengths) {
				if (b) sb.append(String.format("%d,", n));
				++n;
				if (n>m) break;
			}
			sb.append("...");
			System.out.println(sb.toString());
		}
		return new Partition(Arrays.asList(lengthsArray));
	}
	
	/** Create a Markov additive chain by incorporating an i.i.d. text model. */
	public MarkovAdditiveChain createMAC(double[] characterDist) {
		int stateCount = transitionTable.size();
		@SuppressWarnings("unchecked")
		HashMap<Integer, Double>[] preImageList = new HashMap[stateCount];
		
		for (int i=0; i<stateCount; ++i) {
			preImageList[i]=new HashMap<Integer, Double>();
		}	
		
		int source = 0;
		for (int[] transitions : transitionTable) {
			for (int c=0; c<transitions.length; ++c) {
				int target = transitions[c];
				Double prob = preImageList[target].get(source);
				if (prob==null) {
					prob=characterDist[c];
				} else {
					prob+=characterDist[c];
				}
				preImageList[target].put(source, prob);
			}
			++source;
		}
		
		int[][] preimage = new int[stateCount][];
		double[][] preimageProb = new double[stateCount][];
		for (int i=0; i<stateCount; ++i) {
			preimage[i]=new int[preImageList[i].size()];
			preimageProb[i]=new double[preImageList[i].size()];
			int j = 0;
			for (Entry<Integer,Double> e : preImageList[i].entrySet()) {
				preimage[i][j]=e.getKey();
				preimageProb[i][j]=e.getValue();
				++j;
			}
		}
		int[] emissions = new int[stateCount];
		int i=0;
		for (int emission : outputTable) {
			emissions[i]=emission;
			++i;
		}
		return new MarkovAdditiveChain(preimage, preimageProb, emissions);
	}
	
	/** Returns an automaton recognizing the same language, but in a non-overlapping way. */
	// TODO: remove unreachable states
	public CDFA toNonOverlapping() {
		List<int[]> newTransitionTable = new ArrayList<int[]>(transitionTable.size());
		List<Integer> newOutputTable = new ArrayList<Integer>(outputTable.size());
		
		for (int state=0; state<transitionTable.size(); ++state) {
			int[] newTransitions = new int[alphabet.size()];
			if (outputTable.get(state)==0) {
				System.arraycopy(transitionTable.get(state), 0, newTransitions, 0, alphabet.size());
				newOutputTable.add(0);
			} else {
				System.arraycopy(transitionTable.get(0), 0, newTransitions, 0, alphabet.size());
				newOutputTable.add(1);
			}
			newTransitionTable.add(newTransitions);
		}
		
		return new CDFA(alphabet,newTransitionTable,newOutputTable);
	}
	
	/** Returns an automaton recognizing the same language, but returns match positions only (if
	 *  two matches end at the same position, only one is reported. */
	public CDFA toMatchPositionCount() {
		List<int[]> newTransitionTable = new ArrayList<int[]>(transitionTable.size());
		List<Integer> newOutputTable = new ArrayList<Integer>(outputTable.size());
		
		for (int state=0; state<transitionTable.size(); ++state) {
			if (outputTable.get(state)==0) {
				newOutputTable.add(0);
			} else {
				newOutputTable.add(1);
			}
			int[] newTransitions = new int[alphabet.size()];
			System.arraycopy(transitionTable.get(state), 0, newTransitions, 0, alphabet.size());
			newTransitionTable.add(newTransitions);
		}
		return new CDFA(alphabet,newTransitionTable,newOutputTable);
	}
	
	/** Returns a list of states that yield an output > 0. */
	public List<Integer> getOutputStates() {
		List<Integer> result = new ArrayList<Integer>();
		for (int i=0; i<outputTable.size(); ++i) {
			if (outputTable.get(i)>0) {
				result.add(i);
			}
		}
		return result;
	}
	
	public int getStateCount() {
		return outputTable.size();
	}
	
	public String toString() {
		StringBuffer sb = new StringBuffer();
		for (int node=0; node<outputTable.size(); ++node) {
			sb.append(String.format("%d(%d): ", node, outputTable.get(node)));
			for (int c=0; c<alphabet.size(); ++c) {
				char chr = alphabet.get(c);
				sb.append(String.format("%s-->%d, ", chr, transitionTable.get(node)[c]));
			}
			sb.append("\n");
		}
		return sb.toString();
	}
}
